PRISM
=====
Version: 4.5.dev
Date: Sat Apr 03 04:38:25 CEST 2021
Hostname: christopher
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 philosophers-mdp.80.prism philosophers-mdp.80.props --property eat
Parsing model file "philosophers-mdp.80.prism"...
Type: MDP
Modules: phil1 phil2 phil3 phil4 phil5 phil6 phil7 phil8 phil9 phil10 phil11 phil12 phil13 phil14 phil15 phil16 phil17 phil18 phil19 phil20 phil21 phil22 phil23 phil24 phil25 phil26 phil27 phil28 phil29 phil30 phil31 phil32 phil33 phil34 phil35 phil36 phil37 phil38 phil39 phil40 phil41 phil42 phil43 phil44 phil45 phil46 phil47 phil48 phil49 phil50 phil51 phil52 phil53 phil54 phil55 phil56 phil57 phil58 phil59 phil60 phil61 phil62 phil63 phil64 phil65 phil66 phil67 phil68 phil69 phil70 phil71 phil72 phil73 phil74 phil75 phil76 phil77 phil78 phil79 phil80
Variables: p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14 p15 p16 p17 p18 p19 p20 p21 p22 p23 p24 p25 p26 p27 p28 p29 p30 p31 p32 p33 p34 p35 p36 p37 p38 p39 p40 p41 p42 p43 p44 p45 p46 p47 p48 p49 p50 p51 p52 p53 p54 p55 p56 p57 p58 p59 p60 p61 p62 p63 p64 p65 p66 p67 p68 p69 p70 p71 p72 p73 p74 p75 p76 p77 p78 p79 p80
Parsing properties file "philosophers-mdp.80.props"...
1 property:
(1) "eat": Pmax=? [ F ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9))|((p4>=8)&(p4<=9))|((p5>=8)&(p5<=9))|((p6>=8)&(p6<=9))|((p7>=8)&(p7<=9))|((p8>=8)&(p8<=9))|((p9>=8)&(p9<=9))|((p10>=8)&(p10<=9))|((p11>=8)&(p11<=9))|((p12>=8)&(p12<=9))|((p13>=8)&(p13<=9))|((p14>=8)&(p14<=9))|((p15>=8)&(p15<=9))|((p16>=8)&(p16<=9))|((p17>=8)&(p17<=9))|((p18>=8)&(p18<=9))|((p19>=8)&(p19<=9))|((p20>=8)&(p20<=9))|((p21>=8)&(p21<=9))|((p22>=8)&(p22<=9))|((p23>=8)&(p23<=9))|((p24>=8)&(p24<=9))|((p25>=8)&(p25<=9))|((p26>=8)&(p26<=9))|((p27>=8)&(p27<=9))|((p28>=8)&(p28<=9))|((p29>=8)&(p29<=9))|((p30>=8)&(p30<=9))|((p31>=8)&(p31<=9))|((p32>=8)&(p32<=9))|((p33>=8)&(p33<=9))|((p34>=8)&(p34<=9))|((p35>=8)&(p35<=9))|((p36>=8)&(p36<=9))|((p37>=8)&(p37<=9))|((p38>=8)&(p38<=9))|((p39>=8)&(p39<=9))|((p40>=8)&(p40<=9))|((p41>=8)&(p41<=9))|((p42>=8)&(p42<=9))|((p43>=8)&(p43<=9))|((p44>=8)&(p44<=9))|((p45>=8)&(p45<=9))|((p46>=8)&(p46<=9))|((p47>=8)&(p47<=9))|((p48>=8)&(p48<=9))|((p49>=8)&(p49<=9))|((p50>=8)&(p50<=9))|((p51>=8)&(p51<=9))|((p52>=8)&(p52<=9))|((p53>=8)&(p53<=9))|((p54>=8)&(p54<=9))|((p55>=8)&(p55<=9))|((p56>=8)&(p56<=9))|((p57>=8)&(p57<=9))|((p58>=8)&(p58<=9))|((p59>=8)&(p59<=9))|((p60>=8)&(p60<=9))|((p61>=8)&(p61<=9))|((p62>=8)&(p62<=9))|((p63>=8)&(p63<=9))|((p64>=8)&(p64<=9))|((p65>=8)&(p65<=9))|((p66>=8)&(p66<=9))|((p67>=8)&(p67<=9))|((p68>=8)&(p68<=9))|((p69>=8)&(p69<=9))|((p70>=8)&(p70<=9))|((p71>=8)&(p71<=9))|((p72>=8)&(p72<=9))|((p73>=8)&(p73<=9))|((p74>=8)&(p74<=9))|((p75>=8)&(p75<=9))|((p76>=8)&(p76<=9))|((p77>=8)&(p77<=9))|((p78>=8)&(p78<=9))|((p79>=8)&(p79<=9))|((p80>=8)&(p80<=9)) ]
---------------------------------------------------------------------
Model checking: "eat": Pmax=? [ F ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9))|((p4>=8)&(p4<=9))|((p5>=8)&(p5<=9))|((p6>=8)&(p6<=9))|((p7>=8)&(p7<=9))|((p8>=8)&(p8<=9))|((p9>=8)&(p9<=9))|((p10>=8)&(p10<=9))|((p11>=8)&(p11<=9))|((p12>=8)&(p12<=9))|((p13>=8)&(p13<=9))|((p14>=8)&(p14<=9))|((p15>=8)&(p15<=9))|((p16>=8)&(p16<=9))|((p17>=8)&(p17<=9))|((p18>=8)&(p18<=9))|((p19>=8)&(p19<=9))|((p20>=8)&(p20<=9))|((p21>=8)&(p21<=9))|((p22>=8)&(p22<=9))|((p23>=8)&(p23<=9))|((p24>=8)&(p24<=9))|((p25>=8)&(p25<=9))|((p26>=8)&(p26<=9))|((p27>=8)&(p27<=9))|((p28>=8)&(p28<=9))|((p29>=8)&(p29<=9))|((p30>=8)&(p30<=9))|((p31>=8)&(p31<=9))|((p32>=8)&(p32<=9))|((p33>=8)&(p33<=9))|((p34>=8)&(p34<=9))|((p35>=8)&(p35<=9))|((p36>=8)&(p36<=9))|((p37>=8)&(p37<=9))|((p38>=8)&(p38<=9))|((p39>=8)&(p39<=9))|((p40>=8)&(p40<=9))|((p41>=8)&(p41<=9))|((p42>=8)&(p42<=9))|((p43>=8)&(p43<=9))|((p44>=8)&(p44<=9))|((p45>=8)&(p45<=9))|((p46>=8)&(p46<=9))|((p47>=8)&(p47<=9))|((p48>=8)&(p48<=9))|((p49>=8)&(p49<=9))|((p50>=8)&(p50<=9))|((p51>=8)&(p51<=9))|((p52>=8)&(p52<=9))|((p53>=8)&(p53<=9))|((p54>=8)&(p54<=9))|((p55>=8)&(p55<=9))|((p56>=8)&(p56<=9))|((p57>=8)&(p57<=9))|((p58>=8)&(p58<=9))|((p59>=8)&(p59<=9))|((p60>=8)&(p60<=9))|((p61>=8)&(p61<=9))|((p62>=8)&(p62<=9))|((p63>=8)&(p63<=9))|((p64>=8)&(p64<=9))|((p65>=8)&(p65<=9))|((p66>=8)&(p66<=9))|((p67>=8)&(p67<=9))|((p68>=8)&(p68<=9))|((p69>=8)&(p69<=9))|((p70>=8)&(p70<=9))|((p71>=8)&(p71<=9))|((p72>=8)&(p72<=9))|((p73>=8)&(p73<=9))|((p74>=8)&(p74<=9))|((p75>=8)&(p75<=9))|((p76>=8)&(p76<=9))|((p77>=8)&(p77<=9))|((p78>=8)&(p78<=9))|((p79>=8)&(p79<=9))|((p80>=8)&(p80<=9)) ]
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
Computing reachable states...
----------
Computation aborted after 1800.0884053707123 seconds since the total time limit of 1800 seconds was exceeded.